Inference at * 1 2 1 2 
Iof proof for Lemma integer sqrt:



1. n : 
2. 0 < n
3. r : 
4. (r * r)  (n - 1)
5. (n - 1) < ((r+1) * (r+1))
6. (((r+1) * (r+1))  n)
  r:. (((r * r)  n) & (n < ((r+1) * (r+1)))) 

latex

 by With r (D 0) THEN Auto 

latex

 .

Definitions	x:A. B(x), Void, A, False, P  Q, n - m, -n, P & Q, x:A  B(x), A  B, , a < b, n * m, n+m, x:A. B(x), x:AB(x), , {x:A| B(x)} , t  T, #$n
Lemmas	le wf